[Merged by Bors] - chore(Data/Set): split Data/Set/Function #17091
Conversation
b-mehta
added
tech debt
PR summary aa0f8babe1Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for |
Ruben-VandeVelde
added
the
awaiting-author
Co-authored-by: Ruben Van de Velde <[email protected]> Co-authored-by: damiano <[email protected]>
b-mehta
removed
the
awaiting-author
There was a problem hiding this comment.
Can this be under Order? Order.Monotone.Set maybe?
There was a problem hiding this comment.
I'm not convinced by that name - a good chunk of the lemmas in Order.Monotone involve Set anyway, so it's not a good disambiguator. More specifically, what would be the deciding factor for a new lemma going in Order.Monotone.Set as opposed to any one of the other files in Order.Monotone?
There was a problem hiding this comment.
I think there's little to none, which surely is an argument for putting the files close together or even merge them?
There was a problem hiding this comment.
I'm not opposed to putting the files close together, I just don't think Order.Monotone.Set is a good name for the new file!
There was a problem hiding this comment.
Order.Monotone.SetFunction? 🤷
There was a problem hiding this comment.
More importantly, the lemmas in this file use lemmas from Data.Set.Function, which also creates an import cycle.
There was a problem hiding this comment.
See
mathlib4/Mathlib/Order/Monotone/Basic.lean
Line 150 in 809c3fb
, for instance.
Sounds like the "right now" is very outdated
There was a problem hiding this comment.
the lemmas in this file use lemmas from
Data.Set.Function
Where? I don't see any lemma from Data.Set.Function being used. I see definitions being used, but those could move to Data.Set.Operations
There was a problem hiding this comment.
Unfortunately it is not just definitions that are used here, lemmas from Data.Set.Function are used in the file. Furthermore, even if it were only definitions being used, it is out of scope of this PR to additionally move around definitions.
There was a problem hiding this comment.
Okay, but merging was merely a suggestion for how to put the material under Order.Monotone. Please move this new file under Order.Monotone
leanprover-community-mathlib4-bot
added
the
ready-to-merge
Take the lemmas about monotonicity of functions out of Data/Set/Function and move them to Data/Set/Monotone. Also remove `Compl.decidableMem`, as it is already given in `decidableCompl` (instance search already finds it too) Co-authored-by: adomani <[email protected]>
|
Build failed (retrying...): |
Take the lemmas about monotonicity of functions out of Data/Set/Function and move them to Data/Set/Monotone. Also remove `Compl.decidableMem`, as it is already given in `decidableCompl` (instance search already finds it too) Co-authored-by: adomani <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Take the lemmas about monotonicity of functions out of Data/Set/Function and move them to Data/Set/Monotone.
Also remove
Compl.decidableMem, as it is already given indecidableCompl(instance search already finds it too)